Nuprl Lemma : interleaving_sublist
11,40
postcript
pdf
T
:Type,
L
,
L1
,
L2
:(
T
List). interleaving(
T
;
L1
;
L2
;
L
)
L1
L
latex
Definitions
suptype(
S
;
T
)
,
S
T
,
,
t
T
,
x
:
A
.
B
(
x
)
,
disjoint_sublists(
T
;
L1
;
L2
;
L
)
,
P
&
Q
,
L1
L2
,
interleaving(
T
;
L1
;
L2
;
L
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
Lemmas
not
wf
,
nat
wf
,
select
wf
,
non
neg
length
,
length
wf1
,
increasing
wf
,
int
seg
wf
origin
T:Type, L, L1, L2:(T List). interleaving(T;L1;L2;L) 
L1 
L T:Type, L, L1, L2:(T List). interleaving(T;L1;L2;L) L1 L T
T
x:A. B(x) L2 Qx:A. B(x)
}